Trait isotope::term::Value [−][src]
pub trait Value: Debug + Cons + Substitute + Typecheck + HasDependencies + TermEq + Clone { type ValueConsed: From<Self::Consed> + Value; type ValueSubstituted: From<Self::Substituted> + Value;}Show methods
fn into_term_direct(self) -> Term; fn annot(&self) -> Option<AnnotationRef<'_>>; fn is_local_ty(&self) -> Option<bool>; fn is_local_universe(&self) -> Option<bool>; fn is_local_function(&self) -> Option<bool>; fn is_local_pi(&self) -> Option<bool>; fn is_root(&self) -> bool; fn annotate_unchecked(
&self,
annot: Annotation,
ctx: &mut impl ConsCtx + ?Sized
) -> Result<Option<Self::ValueConsed>, Error>; fn is_subtype_in(
&self,
other: &Term,
ctx: &mut impl TermEqCtxMut + ?Sized
) -> Option<bool>; fn code(&self) -> Code; fn untyped_code(&self) -> Code; fn eq_term_in(
&self,
other: &Term,
ctx: &mut impl TermEqCtxMut + ?Sized
) -> Option<bool>; fn form(&self) -> Form; fn id(&self) -> Option<NodeIx> { ... } fn coerce(
&self,
ty: Option<TermId>,
ctx: &mut impl TyCtxMut + ?Sized
) -> Result<Option<Self::ValueConsed>, Error> { ... } fn coerce_id(
&self,
ty: Option<TermId>,
ctx: &mut impl TyCtxMut + ?Sized
) -> Result<Option<TermId>, Error> { ... } fn coerced(
&self,
ty: Option<TermId>,
ctx: &mut impl TyCtxMut + ?Sized
) -> Result<Self::ValueConsed, Error> { ... } fn coerced_id(
&self,
ty: Option<TermId>,
ctx: &mut impl TyCtxMut + ?Sized
) -> Result<TermId, Error> { ... } fn annotate_unchecked_id(
&self,
annot: Annotation,
ctx: &mut impl ConsCtx + ?Sized
) -> Result<Option<TermId>, Error> { ... } fn annotated_unchecked(
&self,
annot: Annotation,
ctx: &mut impl ConsCtx + ?Sized
) -> Result<Self::ValueConsed, Error> { ... } fn annotated_unchecked_id(
&self,
annot: Annotation,
ctx: &mut impl ConsCtx + ?Sized
) -> Result<TermId, Error> { ... } fn is_const(&self) -> bool { ... } fn is_subtype(&self, other: &Term) -> Option<bool> { ... } fn coerce_annot_ty(
&self,
target: &TermId,
ctx: &mut impl TyCtxMut + ?Sized
) -> Result<Option<Annotation>, Error> { ... } fn universe(&self) -> Option<Universe> { ... } fn fn_ty(&self) -> Option<&Pi> { ... } fn subst_rec_id(
&self,
ctx: &mut impl SubstCtx + ?Sized
) -> Result<Option<TermId>, Error> { ... } fn subst_id(
&self,
ctx: &mut impl SubstCtx + ?Sized
) -> Result<Option<TermId>, Error> { ... } fn shift_id(
&self,
n: i32,
base: u32,
ctx: &mut impl ConsCtx + ?Sized
) -> Result<Option<TermId>, Error> { ... } fn shifted_id(
&self,
n: i32,
base: u32,
ctx: &mut impl ConsCtx + ?Sized
) -> Result<TermId, Error> { ... } fn eq_id_in(
&self,
other: &TermId,
ctx: &mut impl TermEqCtxMut + ?Sized
) -> Option<bool> { ... } fn cons_id(&self, ctx: &mut impl ConsCtx + ?Sized) -> Option<TermId> { ... } fn into_id_with(self, ctx: &mut impl ConsCtx + ?Sized) -> TermId { ... } fn ty(&self) -> Option<Cow<'_, Term>> { ... } fn ty_id(&self, ctx: &mut impl ConsCtx + ?Sized) -> Option<Cow<'_, TermId>> { ... } fn diff_ty(&self) -> Option<&TermId> { ... } fn base(&self) -> Option<Cow<'_, Term>> { ... } fn base_id(
&self,
ctx: &mut impl ConsCtx + ?Sized
) -> Option<Cow<'_, TermId>> { ... } fn apply(
&self,
args: &mut SmallVec<[TermId; 2]>,
ctx: &mut impl EvalCtx + ?Sized
) -> Result<Option<TermId>, Error> { ... } fn apply_ty(
&self,
args: &mut SmallVec<[TermId; 2]>,
ctx: &mut impl EvalCtx + ?Sized
) -> Result<Option<TermId>, Error> { ... } fn into_id_direct(self) -> TermId { ... } fn clone_into_id_direct(&self) -> TermId { ... } fn clone_into_id_with(&self, ctx: &mut impl ConsCtx + ?Sized) -> TermId { ... } fn clone_into_term_direct(&self) -> Term { ... } fn into_shallow_cons(self, ctx: &mut impl ConsCtx + ?Sized) -> TermId { ... } fn clone_into_shallow_cons(&self, ctx: &mut impl ConsCtx + ?Sized) -> TermId { ... } fn is_hnf(&self) -> bool { ... } fn is_bnf(&self) -> bool { ... } fn is_enf(&self) -> bool { ... } fn normalize(
&self,
form: Form,
max_steps: u64,
ctx: &mut impl TyCtxMut + ?Sized
) -> Result<Option<TermId>, Error> { ... } fn normalized(
&self,
form: Form,
max_steps: u64,
ctx: &mut impl TyCtxMut + ?Sized
) -> Result<TermId, Error> { ... } fn reduce(
&self,
cfg: impl ReductionConfig,
ctx: &mut impl TyCtxMut + ?Sized
) -> Result<Option<TermId>, Error> { ... } fn reduced(
&self,
cfg: impl ReductionConfig,
ctx: &mut impl TyCtxMut + ?Sized
) -> Result<TermId, Error> { ... } fn reduce_until(
&self,
reduce: impl ReductionConfig,
until: impl TerminationCondition,
ctx: &mut impl TyCtxMut + ?Sized
) -> Result<Option<TermId>, Error> { ... } fn reduced_until(
&self,
reduce: impl ReductionConfig,
until: impl TerminationCondition,
ctx: &mut impl TyCtxMut + ?Sized
) -> Result<TermId, Error> { ... }
Expand description
A trait implemented by values in isotope
’s term language
Associated Types
type ValueConsed: From<Self::Consed> + Value
[src]
type ValueConsed: From<Self::Consed> + Value
[src]The type of value this is consed to
type ValueSubstituted: From<Self::Substituted> + Value
[src]
type ValueSubstituted: From<Self::Substituted> + Value
[src]The type of value this is substituted to
Required methods
fn into_term_direct(self) -> Term
[src]
fn into_term_direct(self) -> Term
[src]Convert this term to a Term
, without any consing
fn annot(&self) -> Option<AnnotationRef<'_>>
[src]
fn annot(&self) -> Option<AnnotationRef<'_>>
[src]Get the type annotation of this term
fn is_local_ty(&self) -> Option<bool>
[src]
fn is_local_ty(&self) -> Option<bool>
[src]Get whether this term is a type
fn is_local_universe(&self) -> Option<bool>
[src]
fn is_local_universe(&self) -> Option<bool>
[src]Get whether this term is a universe
fn is_local_function(&self) -> Option<bool>
[src]
fn is_local_function(&self) -> Option<bool>
[src]Get whether this term is a function
fn is_local_pi(&self) -> Option<bool>
[src]
fn is_local_pi(&self) -> Option<bool>
[src]Get whether this term is a dependent function type
fn annotate_unchecked(
&self,
annot: Annotation,
ctx: &mut impl ConsCtx + ?Sized
) -> Result<Option<Self::ValueConsed>, Error>
[src]
fn annotate_unchecked(
&self,
annot: Annotation,
ctx: &mut impl ConsCtx + ?Sized
) -> Result<Option<Self::ValueConsed>, Error>
[src]Convert this term to an annotation, with only rudimentary type-checking
fn is_subtype_in(
&self,
other: &Term,
ctx: &mut impl TermEqCtxMut + ?Sized
) -> Option<bool>
[src]
fn is_subtype_in(
&self,
other: &Term,
ctx: &mut impl TermEqCtxMut + ?Sized
) -> Option<bool>
[src]Get whether this term is a subtype of another in a given context
Get the hash-code of this term
It is an invariant that, if two terms t
, u
differ only due to typing
annotations for any subterm, t.code().pure() == u.code.pure()
.
fn untyped_code(&self) -> Code
[src]
fn untyped_code(&self) -> Code
[src]Get the hash-code of this term if it was untyped
This can be helpful in, e.g., looking up the untyped term in a hash-map
when one only has the typed term. It is an invariant that, for all terms
t
, t.code().pure() == t.untyped_code().pure()
. On the other hand, it
is not necessarily the case that t.ty() == None
implies that
t.code() == t.untyped_code()
, since while t
itself is not annotated,
it’s subterms may be, which would affect the upper 32 bits of
t.code()
.
fn eq_term_in(
&self,
other: &Term,
ctx: &mut impl TermEqCtxMut + ?Sized
) -> Option<bool>
[src]
fn eq_term_in(
&self,
other: &Term,
ctx: &mut impl TermEqCtxMut + ?Sized
) -> Option<bool>
[src]Compare this term to another within a given context
Provided methods
Get the index of this term in a program graph. Return None
if this term is unindexed
Coerce this term to another type, with type-checking
Coerce this term to another type, with type-checking
Coerce this term to another type, with type-checking
Coerce this term to another type, with type-checking
fn annotate_unchecked_id(
&self,
annot: Annotation,
ctx: &mut impl ConsCtx + ?Sized
) -> Result<Option<TermId>, Error>
[src]
fn annotate_unchecked_id(
&self,
annot: Annotation,
ctx: &mut impl ConsCtx + ?Sized
) -> Result<Option<TermId>, Error>
[src]Convert this term to an annotation, with only rudimentary type-checking
fn annotated_unchecked(
&self,
annot: Annotation,
ctx: &mut impl ConsCtx + ?Sized
) -> Result<Self::ValueConsed, Error>
[src]
fn annotated_unchecked(
&self,
annot: Annotation,
ctx: &mut impl ConsCtx + ?Sized
) -> Result<Self::ValueConsed, Error>
[src]Convert this term to an annotation, with only rudimentary type-checking
fn annotated_unchecked_id(
&self,
annot: Annotation,
ctx: &mut impl ConsCtx + ?Sized
) -> Result<TermId, Error>
[src]
fn annotated_unchecked_id(
&self,
annot: Annotation,
ctx: &mut impl ConsCtx + ?Sized
) -> Result<TermId, Error>
[src]Convert this term to an annotation, with only rudimentary type-checking
fn is_subtype(&self, other: &Term) -> Option<bool>
[src]
fn is_subtype(&self, other: &Term) -> Option<bool>
[src]Get whether this term is a subtype of another in general
fn coerce_annot_ty(
&self,
target: &TermId,
ctx: &mut impl TyCtxMut + ?Sized
) -> Result<Option<Annotation>, Error>
[src]
fn coerce_annot_ty(
&self,
target: &TermId,
ctx: &mut impl TyCtxMut + ?Sized
) -> Result<Option<Annotation>, Error>
[src]Cast this type into another in a given typing context
Substitute this term’s variables recursively given a context
Substitute this term’s variables given a context
Shift this term’s variables with index >= base
up by n
in a given context
Shift this term’s variables with index >= base
up by n
in a given context
Compare this term to a term ID, within a given context
Cons this term within a given context. Return None
if already consed.
fn into_id_with(self, ctx: &mut impl ConsCtx + ?Sized) -> TermId
[src]
fn into_id_with(self, ctx: &mut impl ConsCtx + ?Sized) -> TermId
[src]Convert this term to a TermId
within a given context
Get the type of this term, if any
Get the type of this term, if any
Apply this value, as a function, to a given vector of arguments in a given context
Returns None
if there is no change. Pops off consumed arguments.
Apply this value, as a dependent function type, to a given vector of arguments in a given context
Returns None
if there is no change. Pops off consumed arguments.
fn into_id_direct(self) -> TermId
[src]
fn into_id_direct(self) -> TermId
[src]Convert this term to a TermId
, without any consing
fn clone_into_id_direct(&self) -> TermId
[src]
fn clone_into_id_direct(&self) -> TermId
[src]Clone this term to a TermId
, without any consing
fn clone_into_id_with(&self, ctx: &mut impl ConsCtx + ?Sized) -> TermId
[src]
fn clone_into_id_with(&self, ctx: &mut impl ConsCtx + ?Sized) -> TermId
[src]Clone this term to a TermId
within a given context
fn clone_into_term_direct(&self) -> Term
[src]
fn clone_into_term_direct(&self) -> Term
[src]Clone this term to a Term
without any consing
fn into_shallow_cons(self, ctx: &mut impl ConsCtx + ?Sized) -> TermId
[src]
fn into_shallow_cons(self, ctx: &mut impl ConsCtx + ?Sized) -> TermId
[src]Shallow cons a term directly into a context
fn clone_into_shallow_cons(&self, ctx: &mut impl ConsCtx + ?Sized) -> TermId
[src]
fn clone_into_shallow_cons(&self, ctx: &mut impl ConsCtx + ?Sized) -> TermId
[src]Shallow cons a term directly into a context, cloning if necessary
Convert this term to a normal form
Convert this term a normal form
Convert this term to a normal form, or reduce it up to n
steps
Convert this term a normal form, or reduce it up to n
steps
fn reduce_until(
&self,
reduce: impl ReductionConfig,
until: impl TerminationCondition,
ctx: &mut impl TyCtxMut + ?Sized
) -> Result<Option<TermId>, Error>
[src]
fn reduce_until(
&self,
reduce: impl ReductionConfig,
until: impl TerminationCondition,
ctx: &mut impl TyCtxMut + ?Sized
) -> Result<Option<TermId>, Error>
[src]Convert this term to a normal form, or reduce it up to n
steps
fn reduced_until(
&self,
reduce: impl ReductionConfig,
until: impl TerminationCondition,
ctx: &mut impl TyCtxMut + ?Sized
) -> Result<TermId, Error>
[src]
fn reduced_until(
&self,
reduce: impl ReductionConfig,
until: impl TerminationCondition,
ctx: &mut impl TyCtxMut + ?Sized
) -> Result<TermId, Error>
[src]Convert this term a normal form, or reduce it up to n
steps